GrpSig{i}  GrpSig{[i | j]} 

latex

Up	groups 1
Definitions of Statement	GrpSig
Definitions	t  T, x:A. B(x), GrpSig, S  T
Lemmas	bool wf